\begin{tabbing}
fifo+switch(${\it es}$;$C$;$j$,$i$,$e$.$S_{1}$\=($j$\+
\\[0ex];$i$
\\[0ex];$e$);$j$,$i$,$e$.$S_{2}$\=($j$\+
\\[0ex];$i$
\\[0ex];$e$);$i$,$e$.${\it Req}_{1}$\=($i$\+
\\[0ex];$e$);$j$,$i$,$e$.${\it Ack}_{1}$\=($j$\+
\\[0ex];$i$
\\[0ex];$e$);$i$,$e$.${\it Req}_{2}$\=($i$\+
\\[0ex];$e$);$j$,$i$,$e$.${\it Ack}_{2}$\=($j$\+
\\[0ex];$i$
\\[0ex];$e$))
\-\-\-\-\-\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$i$:$C$, $j$:$C$.\+\+
\\[0ex]$\forall$$x$:es{-}E(${\it es}$), $y$:es{-}E(${\it es}$).
\\[0ex]$S_{2}$($j$;$i$;$x$)
\\[0ex]$\Rightarrow$ $S_{1}$($j$;$i$;$y$)
\\[0ex]$\Rightarrow$ \=((\=es{-}causle(${\it es}$;$x$;$y$)\+\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it req}$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{2}$($j$;$i$;$e$)\} \+
\\[0ex]$\exists$\=${\it ack}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{2}$($j$;$i$;$e$)\} \+
\\[0ex](${\it Req}_{2}$($j$;${\it req}$)
\\[0ex]\& es{-}causle(${\it es}$;$x$;${\it req}$)
\\[0ex]\& es{-}causle(${\it es}$;${\it req}$;${\it ack}$)
\\[0ex]\& es{-}causle(${\it es}$;${\it ack}$;$y$))))
\-\-\-\\[0ex]\& (\=es{-}causle(${\it es}$;$y$;$x$)\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it req}$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{1}$($j$;$i$;$e$)\} \+
\\[0ex]$\exists$\=${\it ack}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{1}$($j$;$i$;$e$)\} \+
\\[0ex](${\it Req}_{1}$($j$;${\it req}$)
\\[0ex]\& es{-}causle(${\it es}$;$y$;${\it req}$)
\\[0ex]\& es{-}causle(${\it es}$;${\it req}$;${\it ack}$)
\\[0ex]\& es{-}causle(${\it es}$;${\it ack}$;$x$))))))
\-\-\-\-\-\\[0ex]\& (\=$\forall$$i$:$C$, $j$:$C$.\+
\\[0ex](\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{1}$($j$;$i$;$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{1}$($j$;$i$;$e$)\} .\+
\\[0ex]($\neg$es{-}causle(${\it es}$;${\it e'}$;$e$)) $\Rightarrow$ es{-}causl(${\it es}$; $e$; ${\it e'}$))
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{2}$($j$;$i$;$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{2}$($j$;$i$;$e$)\} .\+
\\[0ex]($\neg$es{-}causle(${\it es}$;${\it e'}$;$e$)) $\Rightarrow$ es{-}causl(${\it es}$; $e$; ${\it e'}$)))
\-\-\\[0ex]\& (\=$\forall$$i$:$C$, $j$:$C$.\+
\\[0ex](\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{1}$($j$;$i$;$e$) \& ${\it Req}_{1}$($j$;$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{1}$($j$;$i$;$e$) \& ${\it Req}_{1}$($j$;$e$)\} .\+
\\[0ex]($\neg$es{-}causle(${\it es}$;${\it e'}$;$e$)) $\Rightarrow$ es{-}causl(${\it es}$; $e$; ${\it e'}$))
\-\\[0ex]\& (\=$\forall$\=$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{2}$($j$;$i$;$e$) \& ${\it Req}_{2}$($j$;$e$)\} ,\+\+
\\[0ex]${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{2}$($j$;$i$;$e$) \& ${\it Req}_{2}$($j$;$e$)\} .
\-\\[0ex]($\neg$es{-}causle(${\it es}$;${\it e'}$;$e$)) $\Rightarrow$ es{-}causl(${\it es}$; $e$; ${\it e'}$)))
\-\-\\[0ex]\& (\=$\forall$$i$:$C$, $j$:$C$.\+
\\[0ex](\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{1}$($j$;$i$;$e$) \& ${\it Req}_{1}$($j$;$e$)\} , ${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{1}$($j$;$i$;$e$) \& ${\it Req}_{1}$($j$;$e$)\} .\+
\\[0ex]es{-}causl(${\it es}$; $e$; ${\it e'}$)
\\[0ex]$\Rightarrow$ ($\exists$$a$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{1}$($j$;$i$;$e$)\} . (es{-}causl(${\it es}$; $e$; $a$) \& es{-}causl(${\it es}$; $a$; ${\it e'}$))))
\-\\[0ex]\& (\=$\forall$\=$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{2}$($j$;$i$;$e$) \& ${\it Req}_{2}$($j$;$e$)\} ,\+\+
\\[0ex]${\it e'}$:\{$e$:es{-}E(${\it es}$)$\mid$ $S_{2}$($j$;$i$;$e$) \& ${\it Req}_{2}$($j$;$e$)\} .
\-\\[0ex]es{-}causl(${\it es}$; $e$; ${\it e'}$)
\\[0ex]$\Rightarrow$ ($\exists$\=$a$:\{$e$:es{-}E(${\it es}$)$\mid$ ${\it Ack}_{2}$($j$;$i$;$e$)\} \+
\\[0ex](es{-}causl(${\it es}$; $e$; $a$) \& es{-}causl(${\it es}$; $a$; ${\it e'}$)))))
\-\-\-\-
\end{tabbing}